$\forall$${\it es}$:ES, ${\it Config}$:AbsInterface(chain\_config()), ${\it Cmd}$:Type, ${\it Sys}$:AbsInterface(chain\_sys(${\it Cmd}$)).
\\[0ex]valid{-}sys{-}dcdr\{i:l\}(${\it es}$;${\it Config}$;${\it Cmd}$;${\it Sys}$)
\\[0ex]$\in$ $e$:E$\rightarrow$Dec(($\uparrow$($e$ $\in_{b}$ ${\it Sys}$)) c$\wedge$ valid{-}sys(${\it es}$;${\it Config}$;${\it Sys}$;$e$))